YES 12.259 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule List
  ((group :: [Int]  ->  [[Int]]) :: [Int]  ->  [[Int]])

module List where
  import qualified Maybe
import qualified Prelude

  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy _ [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = (\(ys,_) ->ys) vv10
zs = (\(_,zs) ->zs) vv10


module Maybe where
  import qualified List
import qualified Prelude



Lambda Reductions:
The following Lambda expression
\(_,zs)→zs

is transformed to
zs0 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys0 (ys,_) = ys

The following Lambda expression
\(_,zs)→zs

is transformed to
zs1 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys1 (ys,_) = ys



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR

mainModule List
  ((group :: [Int]  ->  [[Int]]) :: [Int]  ->  [[Int]])

module List where
  import qualified Maybe
import qualified Prelude

  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy _ [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = ys0 vv10
ys0 (ys,_) = ys
zs = zs0 vv10
zs0 (_,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
xs@(ww : wx)

is replaced by the following term
ww : wx



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR

mainModule List
  ((group :: [Int]  ->  [[Int]]) :: [Int]  ->  [[Int]])

module List where
  import qualified Maybe
import qualified Prelude

  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = ys0 vv10
ys0 (ys,vx) = ys
zs = zs0 vv10
zs0 (vy,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
span p [] = ([],[])
span p (ww : wx)
 | p ww
 = (ww : ys,zs)
 | otherwise
 = ([],ww : wx)
where 
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

is transformed to
span p [] = span3 p []
span p (ww : wx) = span2 p (ww : wx)

span2 p (ww : wx) = 
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

span3 p [] = ([],[])
span3 xx xy = span2 xx xy



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed

mainModule List
  ((group :: [Int]  ->  [[Int]]) :: [Int]  ->  [[Int]])

module List where
  import qualified Maybe
import qualified Prelude

  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = ys0 vv10
ys0 (ys,vx) = ys
zs = zs0 vv10
zs0 (vy,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
(x : ys) : groupBy eq zs
where 
vv10  = span (eq x) xs
ys  = ys0 vv10
ys0 (ys,vx) = ys
zs  = zs0 vv10
zs0 (vy,zs) = zs

are unpacked to the following functions on top level
groupByYs0 xz yu yv (ys,vx) = ys

groupByZs0 xz yu yv (vy,zs) = zs

groupByYs xz yu yv = groupByYs0 xz yu yv (groupByVv10 xz yu yv)

groupByVv10 xz yu yv = span (xz yu) yv

groupByZs xz yu yv = groupByZs0 xz yu yv (groupByVv10 xz yu yv)

The bindings of the following Let/Where expression
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

are unpacked to the following functions on top level
span2Ys yw yx = span2Ys1 yw yx (span2Vu43 yw yx)

span2Zs yw yx = span2Zs1 yw yx (span2Vu43 yw yx)

span2Zs1 yw yx (wy,zs) = zs

span2Span0 yw yx p ww wx True = ([],ww : wx)

span2Span1 yw yx p ww wx True = (ww : span2Ys yw yx,span2Zs yw yx)
span2Span1 yw yx p ww wx False = span2Span0 yw yx p ww wx otherwise

span2Vu43 yw yx = span yw yx

span2Ys1 yw yx (ys,wz) = ys



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow

mainModule List
  (group :: [Int]  ->  [[Int]])

module List where
  import qualified Maybe
import qualified Prelude

  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = (x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs)

  
groupByVv10 xz yu yv = span (xz yu) yv

  
groupByYs xz yu yv = groupByYs0 xz yu yv (groupByVv10 xz yu yv)

  
groupByYs0 xz yu yv (ys,vx) = ys

  
groupByZs xz yu yv = groupByZs0 xz yu yv (groupByVv10 xz yu yv)

  
groupByZs0 xz yu yv (vy,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Ys(:(Pos(Zero), yy3111)) → new_span2Ys(yy3111)
new_span2Ys(:(Neg(Zero), yy3111)) → new_span2Ys(yy3111)
new_span2Zs(:(Pos(Zero), yy3111)) → new_span2Ys(yy3111)
new_span2Zs(:(Neg(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Ys(:(Neg(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Zs(:(Pos(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Ys(:(Pos(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Zs(:(Neg(Zero), yy3111)) → new_span2Ys(yy3111)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Zs1(yy376, yy377, yy378, Zero, Zero) → new_span2Zs0(yy376, yy378)
new_span2Ys1(yy370, yy371, yy372, Zero, Zero) → new_span2Zs0(yy370, yy372)
new_span2Zs1(yy376, yy377, yy378, Zero, Zero) → new_span2Ys0(yy376, yy378)
new_span2Zs0(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs1(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys0(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys1(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs1(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs1(yy376, yy377, yy378, yy3790, yy3800)
new_span2Ys1(yy370, yy371, yy372, Zero, Zero) → new_span2Ys0(yy370, yy372)
new_span2Ys1(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys1(yy370, yy371, yy372, yy3730, yy3740)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_groupByZs0(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs0(yy189, yy190, yy191, yy1920, yy1930)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_groupByYs0(yy142, yy143, yy144, Succ(yy1450), Succ(yy1460)) → new_groupByYs0(yy142, yy143, yy144, yy1450, yy1460)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Zs2(:(Pos(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Zs2(:(Neg(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Ys2(:(Pos(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Ys2(:(Neg(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Ys2(:(Neg(Zero), yy3111)) → new_span2Ys2(yy3111)
new_span2Zs2(:(Pos(Zero), yy3111)) → new_span2Ys2(yy3111)
new_span2Zs2(:(Neg(Zero), yy3111)) → new_span2Ys2(yy3111)
new_span2Ys2(:(Pos(Zero), yy3111)) → new_span2Ys2(yy3111)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Ys10(yy358, yy359, yy360, Zero, Zero) → new_span2Zs3(yy358, yy360)
new_span2Ys3(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys10(yy69, yy71000, yy711, yy69, yy71000)
new_span2Zs3(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs10(yy76, yy77000, yy771, yy76, yy77000)
new_span2Zs10(yy364, yy365, yy366, Zero, Zero) → new_span2Ys3(yy364, yy366)
new_span2Zs10(yy364, yy365, yy366, Zero, Zero) → new_span2Zs3(yy364, yy366)
new_span2Ys10(yy358, yy359, yy360, Zero, Zero) → new_span2Ys3(yy358, yy360)
new_span2Zs10(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs10(yy364, yy365, yy366, yy3670, yy3680)
new_span2Ys10(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys10(yy358, yy359, yy360, yy3610, yy3620)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_groupByZs00(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs00(yy183, yy184, yy185, yy1860, yy1870)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_groupByYs00(yy136, yy137, yy138, Succ(yy1390), Succ(yy1400)) → new_groupByYs00(yy136, yy137, yy138, yy1390, yy1400)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_groupBy(:(yy30, yy31)) → new_groupBy(new_groupByZs01(yy30, yy31))

The TRS R consists of the following rules:

new_span2Ys6(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys17(yy69, yy71000, yy711, yy69, yy71000)
new_span2Ys6(yy69, []) → []
new_span2Ys110(yy3111, yy11, yy10) → :(Neg(Zero), yy11)
new_span2Zs13(yy376, yy377, yy378, yy388, yy387) → yy387
new_span2Ys11(yy3111, yy5, yy4) → :(Pos(Zero), yy5)
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs14(yy364, yy365, yy366, yy3670, yy3680)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys17(yy358, yy359, yy360, yy3610, yy3620)
new_span2Zs7(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys13(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs16(yy3111, yy13, yy12) → yy12
new_span2Ys7(:(Neg(Zero), yy3111)) → new_span2Ys110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Zs110(yy3111, yy17, yy16) → yy16
new_groupByZs03(yy189, yy190, yy191, Zero, Zero) → new_groupByZs04(yy189, yy190, yy191, new_span2Ys4(yy189, yy191), new_span2Zs4(yy189, yy191))
new_groupByZs01(yy30, []) → []
new_span2Ys6(yy69, :(Neg(yy7100), yy711)) → []
new_span2Ys17(yy358, yy359, yy360, Zero, Succ(yy3620)) → new_span2Ys18(yy358, yy359, yy360)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Zero) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs7(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Pos(yy6700), yy671)) → []
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Succ(yy31000)), yy311)) → new_groupByZs03(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys15(yy370, yy371, yy372, yy386, yy385) → :(Neg(Succ(yy371)), yy386)
new_span2Ys7(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs4(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs11(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys16(yy358, yy359, yy360, yy382, yy381) → :(Pos(Succ(yy359)), yy382)
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs03(yy189, yy190, yy191, yy1920, yy1930)
new_groupByZs01(Pos(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_span2Ys13(yy370, yy371, yy372, Zero, Succ(yy3740)) → new_span2Ys14(yy370, yy371, yy372)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Zero) → new_span2Ys14(yy370, yy371, yy372)
new_span2Zs4(yy82, :(Neg(Zero), yy831)) → :(Neg(Zero), yy831)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs05(yy183, yy184, yy185, yy1860, yy1870)
new_span2Ys5(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs5([]) → []
new_span2Zs14(yy364, yy365, yy366, Zero, Zero) → new_span2Zs19(yy364, yy365, yy366, new_span2Ys6(yy364, yy366), new_span2Zs6(yy364, yy366))
new_groupByZs01(Pos(Succ(yy3000)), :(Neg(yy3100), yy311)) → :(Neg(yy3100), yy311)
new_groupByZs01(Neg(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs02(yy189, yy190, yy191) → :(Neg(Succ(yy190)), yy191)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Zero), yy311)) → :(Neg(Zero), yy311)
new_span2Zs7(:(Neg(Zero), yy3111)) → new_span2Zs15(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys19(yy3111, yy9, yy8) → :(Pos(Zero), yy9)
new_groupByZs01(Neg(Zero), :(Neg(Zero), yy311)) → new_span2Zs7(yy311)
new_groupByZs05(yy183, yy184, yy185, Zero, Succ(yy1870)) → new_groupByZs06(yy183, yy184, yy185)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Zero) → new_groupByZs06(yy183, yy184, yy185)
new_span2Zs17(yy3111, yy15, yy14) → yy14
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Zero) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs14(yy364, yy365, yy366, Zero, Succ(yy3680)) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs6(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs14(yy76, yy77000, yy771, yy76, yy77000)
new_span2Zs5(:(Pos(Zero), yy3111)) → new_span2Zs16(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys18(yy358, yy359, yy360) → []
new_span2Ys5(:(Neg(Zero), yy3111)) → new_span2Ys12(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs5(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Zs19(yy364, yy365, yy366, yy384, yy383) → yy383
new_span2Zs7(:(Pos(Zero), yy3111)) → new_span2Zs110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_groupByZs01(Neg(Zero), :(Pos(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Ys17(yy358, yy359, yy360, Zero, Zero) → new_span2Ys16(yy358, yy359, yy360, new_span2Ys6(yy358, yy360), new_span2Zs6(yy358, yy360))
new_span2Zs11(yy376, yy377, yy378, Zero, Succ(yy3800)) → new_span2Zs12(yy376, yy377, yy378)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Zero) → new_span2Zs12(yy376, yy377, yy378)
new_span2Ys6(yy69, :(Pos(Zero), yy711)) → []
new_groupByZs06(yy183, yy184, yy185) → :(Pos(Succ(yy184)), yy185)
new_span2Zs11(yy376, yy377, yy378, Zero, Zero) → new_span2Zs13(yy376, yy377, yy378, new_span2Ys4(yy376, yy378), new_span2Zs4(yy376, yy378))
new_span2Zs4(yy82, :(Pos(yy8300), yy831)) → :(Pos(yy8300), yy831)
new_span2Zs6(yy76, :(Neg(yy7700), yy771)) → :(Neg(yy7700), yy771)
new_span2Zs5(:(Neg(Zero), yy3111)) → new_span2Zs17(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_groupByZs01(Pos(Zero), :(Neg(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Zs12(yy376, yy377, yy378) → :(Neg(Succ(yy377)), yy378)
new_span2Ys7(:(Pos(Zero), yy3111)) → new_span2Ys19(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys5([]) → []
new_groupByZs05(yy183, yy184, yy185, Zero, Zero) → new_groupByZs07(yy183, yy184, yy185, new_span2Ys6(yy183, yy185), new_span2Zs6(yy183, yy185))
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Zero) → new_groupByZs02(yy189, yy190, yy191)
new_groupByZs03(yy189, yy190, yy191, Zero, Succ(yy1930)) → new_groupByZs02(yy189, yy190, yy191)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys13(yy370, yy371, yy372, yy3730, yy3740)
new_span2Zs7([]) → []
new_groupByZs04(yy189, yy190, yy191, yy201, yy200) → yy200
new_span2Ys12(yy3111, yy7, yy6) → :(Neg(Zero), yy7)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs11(yy376, yy377, yy378, yy3790, yy3800)
new_span2Ys4(yy66, []) → []
new_span2Ys7([]) → []
new_span2Zs18(yy364, yy365, yy366) → :(Pos(Succ(yy365)), yy366)
new_groupByZs01(Neg(Succ(yy3000)), :(Pos(yy3100), yy311)) → :(Pos(yy3100), yy311)
new_span2Zs4(yy82, []) → []
new_span2Ys5(:(Pos(Zero), yy3111)) → new_span2Ys11(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs6(yy76, []) → []
new_span2Ys13(yy370, yy371, yy372, Zero, Zero) → new_span2Ys15(yy370, yy371, yy372, new_span2Ys4(yy370, yy372), new_span2Zs4(yy370, yy372))
new_span2Ys7(:(Pos(Succ(yy311000)), yy3111)) → []
new_groupByZs07(yy183, yy184, yy185, yy199, yy198) → yy198
new_span2Zs6(yy76, :(Pos(Zero), yy771)) → :(Pos(Zero), yy771)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Succ(yy31000)), yy311)) → new_groupByZs05(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Zs5(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs01(Neg(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Zero), yy311)) → :(Pos(Zero), yy311)
new_span2Ys5(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Ys14(yy370, yy371, yy372) → []
new_groupByZs01(Pos(Zero), :(Pos(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Ys4(yy66, :(Neg(Zero), yy671)) → []
new_span2Zs15(yy3111, yy19, yy18) → yy18
new_groupByZs01(Pos(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)

The set Q consists of the following terms:

new_span2Zs15(x0, x1, x2)
new_span2Zs7([])
new_span2Zs14(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys17(x0, x1, x2, Zero, Succ(x3))
new_span2Ys6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys12(x0, x1, x2)
new_span2Zs4(x0, [])
new_span2Zs18(x0, x1, x2)
new_span2Zs11(x0, x1, x2, Zero, Succ(x3))
new_span2Zs110(x0, x1, x2)
new_span2Zs7(:(Pos(Succ(x0)), x1))
new_span2Ys14(x0, x1, x2)
new_span2Zs5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Succ(x3), Zero)
new_span2Ys5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Zero, Zero)
new_span2Zs19(x0, x1, x2, x3, x4)
new_span2Ys7([])
new_span2Ys11(x0, x1, x2)
new_groupByZs01(Pos(Zero), :(Pos(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Succ(x3))
new_span2Zs7(:(Neg(Zero), x0))
new_span2Zs14(x0, x1, x2, Succ(x3), Zero)
new_span2Ys110(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Zero), :(Pos(Zero), x0))
new_groupByZs07(x0, x1, x2, x3, x4)
new_span2Zs5(:(Neg(Succ(x0)), x1))
new_groupByZs02(x0, x1, x2)
new_span2Ys7(:(Pos(Succ(x0)), x1))
new_span2Ys4(x0, :(Pos(x1), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Neg(Zero), x0))
new_span2Zs13(x0, x1, x2, x3, x4)
new_span2Ys16(x0, x1, x2, x3, x4)
new_span2Zs4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys7(:(Neg(Succ(x0)), x1))
new_span2Ys7(:(Neg(Zero), x0))
new_span2Ys17(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Succ(x0)), :(Pos(x1), x2))
new_groupByZs01(Neg(Succ(x0)), :(Neg(Succ(x1)), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Succ(x4))
new_groupByZs05(x0, x1, x2, Zero, Succ(x3))
new_span2Ys5(:(Neg(Zero), x0))
new_span2Ys19(x0, x1, x2)
new_span2Zs5(:(Pos(Zero), x0))
new_groupByZs01(Pos(Succ(x0)), :(Pos(Zero), x1))
new_groupByZs05(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys4(x0, :(Neg(Zero), x1))
new_span2Ys5(:(Neg(Succ(x0)), x1))
new_groupByZs01(Neg(Zero), :(Neg(Succ(x0)), x1))
new_span2Ys6(x0, [])
new_groupByZs01(Neg(Succ(x0)), :(Neg(Zero), x1))
new_span2Ys6(x0, :(Neg(x1), x2))
new_span2Zs12(x0, x1, x2)
new_groupByZs01(Neg(Zero), :(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Zero)
new_span2Zs11(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs16(x0, x1, x2)
new_span2Ys5(:(Pos(Zero), x0))
new_span2Ys6(x0, :(Pos(Zero), x1))
new_span2Zs17(x0, x1, x2)
new_span2Ys4(x0, [])
new_groupByZs01(x0, [])
new_span2Zs4(x0, :(Pos(x1), x2))
new_span2Zs6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys13(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys5([])
new_span2Zs6(x0, [])
new_span2Ys7(:(Pos(Zero), x0))
new_span2Ys17(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Neg(Zero), :(Pos(Succ(x0)), x1))
new_span2Ys17(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs4(x0, :(Neg(Zero), x1))
new_groupByZs06(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Succ(x0)), :(Neg(x1), x2))
new_span2Zs14(x0, x1, x2, Zero, Succ(x3))
new_groupByZs01(Pos(Zero), :(Neg(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Zero)
new_span2Ys13(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Pos(Zero), x0))
new_span2Zs5([])
new_span2Zs7(:(Pos(Zero), x0))
new_span2Ys15(x0, x1, x2, x3, x4)
new_groupByZs01(Pos(Succ(x0)), :(Pos(Succ(x1)), x2))
new_span2Zs14(x0, x1, x2, Zero, Zero)
new_groupByZs04(x0, x1, x2, x3, x4)
new_span2Zs6(x0, :(Pos(Zero), x1))
new_span2Zs6(x0, :(Neg(x1), x2))
new_span2Ys4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys18(x0, x1, x2)
new_span2Zs7(:(Neg(Succ(x0)), x1))
new_span2Zs5(:(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Succ(x3))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_groupBy(:(yy30, yy31)) → new_groupBy(new_groupByZs01(yy30, yy31))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x1, x2)) = 1 + x2   
POL(Neg(x1)) = 0   
POL(Pos(x1)) = 0   
POL(Succ(x1)) = 0   
POL(Zero) = 0   
POL([]) = 0   
POL(new_groupBy(x1)) = x1   
POL(new_groupByZs01(x1, x2)) = x2   
POL(new_groupByZs02(x1, x2, x3)) = 1 + x3   
POL(new_groupByZs03(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_groupByZs04(x1, x2, x3, x4, x5)) = x5   
POL(new_groupByZs05(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_groupByZs06(x1, x2, x3)) = 1 + x3   
POL(new_groupByZs07(x1, x2, x3, x4, x5)) = x5   
POL(new_span2Ys11(x1, x2, x3)) = 1 + x2   
POL(new_span2Ys110(x1, x2, x3)) = 1 + x2   
POL(new_span2Ys12(x1, x2, x3)) = 1 + x2   
POL(new_span2Ys13(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Ys14(x1, x2, x3)) = 0   
POL(new_span2Ys15(x1, x2, x3, x4, x5)) = 1 + x4   
POL(new_span2Ys16(x1, x2, x3, x4, x5)) = 1 + x4   
POL(new_span2Ys17(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Ys18(x1, x2, x3)) = 0   
POL(new_span2Ys19(x1, x2, x3)) = 1 + x2   
POL(new_span2Ys4(x1, x2)) = x2   
POL(new_span2Ys5(x1)) = x1   
POL(new_span2Ys6(x1, x2)) = x2   
POL(new_span2Ys7(x1)) = x1   
POL(new_span2Zs11(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Zs110(x1, x2, x3)) = x3   
POL(new_span2Zs12(x1, x2, x3)) = 1 + x3   
POL(new_span2Zs13(x1, x2, x3, x4, x5)) = 1 + x5   
POL(new_span2Zs14(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Zs15(x1, x2, x3)) = x3   
POL(new_span2Zs16(x1, x2, x3)) = x3   
POL(new_span2Zs17(x1, x2, x3)) = 1 + x3   
POL(new_span2Zs18(x1, x2, x3)) = 1 + x3   
POL(new_span2Zs19(x1, x2, x3, x4, x5)) = x5   
POL(new_span2Zs4(x1, x2)) = x2   
POL(new_span2Zs5(x1)) = x1   
POL(new_span2Zs6(x1, x2)) = x2   
POL(new_span2Zs7(x1)) = x1   

The following usable rules [17] were oriented:

new_span2Ys4(yy66, :(Pos(yy6700), yy671)) → []
new_span2Zs7(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs04(yy189, yy190, yy191, yy201, yy200) → yy200
new_groupByZs06(yy183, yy184, yy185) → :(Pos(Succ(yy184)), yy185)
new_span2Zs17(yy3111, yy15, yy14) → yy14
new_span2Ys4(yy66, []) → []
new_groupByZs01(yy30, []) → []
new_span2Ys16(yy358, yy359, yy360, yy382, yy381) → :(Pos(Succ(yy359)), yy382)
new_groupByZs01(Neg(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Zero) → new_groupByZs06(yy183, yy184, yy185)
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs03(yy189, yy190, yy191, yy1920, yy1930)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys13(yy370, yy371, yy372, yy3730, yy3740)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Zero), yy311)) → :(Pos(Zero), yy311)
new_span2Zs14(yy364, yy365, yy366, Zero, Succ(yy3680)) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs4(yy82, :(Pos(yy8300), yy831)) → :(Pos(yy8300), yy831)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs05(yy183, yy184, yy185, yy1860, yy1870)
new_span2Ys14(yy370, yy371, yy372) → []
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys17(yy358, yy359, yy360, yy3610, yy3620)
new_span2Zs7(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Zs5(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs01(Pos(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_span2Ys5(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Zs13(yy376, yy377, yy378, yy388, yy387) → yy387
new_span2Ys13(yy370, yy371, yy372, Zero, Zero) → new_span2Ys15(yy370, yy371, yy372, new_span2Ys4(yy370, yy372), new_span2Zs4(yy370, yy372))
new_span2Zs5(:(Pos(Zero), yy3111)) → new_span2Zs16(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs5([]) → []
new_span2Zs4(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs11(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys6(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys17(yy69, yy71000, yy711, yy69, yy71000)
new_span2Ys12(yy3111, yy7, yy6) → :(Neg(Zero), yy7)
new_groupByZs05(yy183, yy184, yy185, Zero, Succ(yy1870)) → new_groupByZs06(yy183, yy184, yy185)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Zero) → new_span2Zs12(yy376, yy377, yy378)
new_span2Ys4(yy66, :(Neg(Zero), yy671)) → []
new_span2Zs6(yy76, :(Neg(yy7700), yy771)) → :(Neg(yy7700), yy771)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Succ(yy31000)), yy311)) → new_groupByZs03(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys5(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs6(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs14(yy76, yy77000, yy771, yy76, yy77000)
new_groupByZs01(Pos(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs01(Pos(Zero), :(Neg(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Ys6(yy69, :(Pos(Zero), yy711)) → []
new_span2Zs7(:(Pos(Zero), yy3111)) → new_span2Zs110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys6(yy69, []) → []
new_span2Ys15(yy370, yy371, yy372, yy386, yy385) → :(Neg(Succ(yy371)), yy386)
new_span2Zs18(yy364, yy365, yy366) → :(Pos(Succ(yy365)), yy366)
new_span2Ys110(yy3111, yy11, yy10) → :(Neg(Zero), yy11)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Succ(yy31000)), yy311)) → new_groupByZs05(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys5([]) → []
new_span2Ys7(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Ys7([]) → []
new_span2Zs5(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_groupByZs01(Neg(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs05(yy183, yy184, yy185, Zero, Zero) → new_groupByZs07(yy183, yy184, yy185, new_span2Ys6(yy183, yy185), new_span2Zs6(yy183, yy185))
new_span2Ys7(:(Neg(Zero), yy3111)) → new_span2Ys110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys17(yy358, yy359, yy360, Zero, Succ(yy3620)) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs12(yy376, yy377, yy378) → :(Neg(Succ(yy377)), yy378)
new_groupByZs02(yy189, yy190, yy191) → :(Neg(Succ(yy190)), yy191)
new_span2Zs19(yy364, yy365, yy366, yy384, yy383) → yy383
new_span2Ys7(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Ys11(yy3111, yy5, yy4) → :(Pos(Zero), yy5)
new_groupByZs01(Neg(Succ(yy3000)), :(Pos(yy3100), yy311)) → :(Pos(yy3100), yy311)
new_groupByZs03(yy189, yy190, yy191, Zero, Succ(yy1930)) → new_groupByZs02(yy189, yy190, yy191)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Zero), yy311)) → :(Neg(Zero), yy311)
new_span2Zs7(:(Neg(Zero), yy3111)) → new_span2Zs15(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_groupByZs01(Pos(Zero), :(Pos(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Zs15(yy3111, yy19, yy18) → yy18
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs14(yy364, yy365, yy366, yy3670, yy3680)
new_span2Zs5(:(Neg(Zero), yy3111)) → new_span2Zs17(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Zero) → new_span2Ys14(yy370, yy371, yy372)
new_groupByZs01(Neg(Zero), :(Pos(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Zs6(yy76, []) → []
new_span2Ys13(yy370, yy371, yy372, Zero, Succ(yy3740)) → new_span2Ys14(yy370, yy371, yy372)
new_span2Zs7([]) → []
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Zero) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs14(yy364, yy365, yy366, Zero, Zero) → new_span2Zs19(yy364, yy365, yy366, new_span2Ys6(yy364, yy366), new_span2Zs6(yy364, yy366))
new_span2Ys5(:(Pos(Zero), yy3111)) → new_span2Ys11(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys18(yy358, yy359, yy360) → []
new_span2Zs11(yy376, yy377, yy378, Zero, Succ(yy3800)) → new_span2Zs12(yy376, yy377, yy378)
new_groupByZs01(Neg(Zero), :(Neg(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Zs4(yy82, []) → []
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Zero) → new_groupByZs02(yy189, yy190, yy191)
new_span2Ys4(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys13(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs4(yy82, :(Neg(Zero), yy831)) → :(Neg(Zero), yy831)
new_span2Zs16(yy3111, yy13, yy12) → yy12
new_span2Ys6(yy69, :(Neg(yy7100), yy711)) → []
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs11(yy376, yy377, yy378, yy3790, yy3800)
new_groupByZs07(yy183, yy184, yy185, yy199, yy198) → yy198
new_span2Ys5(:(Neg(Zero), yy3111)) → new_span2Ys12(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_groupByZs03(yy189, yy190, yy191, Zero, Zero) → new_groupByZs04(yy189, yy190, yy191, new_span2Ys4(yy189, yy191), new_span2Zs4(yy189, yy191))
new_span2Ys17(yy358, yy359, yy360, Zero, Zero) → new_span2Ys16(yy358, yy359, yy360, new_span2Ys6(yy358, yy360), new_span2Zs6(yy358, yy360))
new_span2Ys19(yy3111, yy9, yy8) → :(Pos(Zero), yy9)
new_span2Zs6(yy76, :(Pos(Zero), yy771)) → :(Pos(Zero), yy771)
new_groupByZs01(Pos(Succ(yy3000)), :(Neg(yy3100), yy311)) → :(Neg(yy3100), yy311)
new_span2Ys7(:(Pos(Zero), yy3111)) → new_span2Ys19(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Zero) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs11(yy376, yy377, yy378, Zero, Zero) → new_span2Zs13(yy376, yy377, yy378, new_span2Ys4(yy376, yy378), new_span2Zs4(yy376, yy378))
new_span2Zs110(yy3111, yy17, yy16) → yy16



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_span2Ys6(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys17(yy69, yy71000, yy711, yy69, yy71000)
new_span2Ys6(yy69, []) → []
new_span2Ys110(yy3111, yy11, yy10) → :(Neg(Zero), yy11)
new_span2Zs13(yy376, yy377, yy378, yy388, yy387) → yy387
new_span2Ys11(yy3111, yy5, yy4) → :(Pos(Zero), yy5)
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs14(yy364, yy365, yy366, yy3670, yy3680)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys17(yy358, yy359, yy360, yy3610, yy3620)
new_span2Zs7(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys13(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs16(yy3111, yy13, yy12) → yy12
new_span2Ys7(:(Neg(Zero), yy3111)) → new_span2Ys110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Zs110(yy3111, yy17, yy16) → yy16
new_groupByZs03(yy189, yy190, yy191, Zero, Zero) → new_groupByZs04(yy189, yy190, yy191, new_span2Ys4(yy189, yy191), new_span2Zs4(yy189, yy191))
new_groupByZs01(yy30, []) → []
new_span2Ys6(yy69, :(Neg(yy7100), yy711)) → []
new_span2Ys17(yy358, yy359, yy360, Zero, Succ(yy3620)) → new_span2Ys18(yy358, yy359, yy360)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Zero) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs7(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Pos(yy6700), yy671)) → []
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Succ(yy31000)), yy311)) → new_groupByZs03(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys15(yy370, yy371, yy372, yy386, yy385) → :(Neg(Succ(yy371)), yy386)
new_span2Ys7(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs4(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs11(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys16(yy358, yy359, yy360, yy382, yy381) → :(Pos(Succ(yy359)), yy382)
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs03(yy189, yy190, yy191, yy1920, yy1930)
new_groupByZs01(Pos(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_span2Ys13(yy370, yy371, yy372, Zero, Succ(yy3740)) → new_span2Ys14(yy370, yy371, yy372)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Zero) → new_span2Ys14(yy370, yy371, yy372)
new_span2Zs4(yy82, :(Neg(Zero), yy831)) → :(Neg(Zero), yy831)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs05(yy183, yy184, yy185, yy1860, yy1870)
new_span2Ys5(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs5([]) → []
new_span2Zs14(yy364, yy365, yy366, Zero, Zero) → new_span2Zs19(yy364, yy365, yy366, new_span2Ys6(yy364, yy366), new_span2Zs6(yy364, yy366))
new_groupByZs01(Pos(Succ(yy3000)), :(Neg(yy3100), yy311)) → :(Neg(yy3100), yy311)
new_groupByZs01(Neg(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs02(yy189, yy190, yy191) → :(Neg(Succ(yy190)), yy191)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Zero), yy311)) → :(Neg(Zero), yy311)
new_span2Zs7(:(Neg(Zero), yy3111)) → new_span2Zs15(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys19(yy3111, yy9, yy8) → :(Pos(Zero), yy9)
new_groupByZs01(Neg(Zero), :(Neg(Zero), yy311)) → new_span2Zs7(yy311)
new_groupByZs05(yy183, yy184, yy185, Zero, Succ(yy1870)) → new_groupByZs06(yy183, yy184, yy185)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Zero) → new_groupByZs06(yy183, yy184, yy185)
new_span2Zs17(yy3111, yy15, yy14) → yy14
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Zero) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs14(yy364, yy365, yy366, Zero, Succ(yy3680)) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs6(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs14(yy76, yy77000, yy771, yy76, yy77000)
new_span2Zs5(:(Pos(Zero), yy3111)) → new_span2Zs16(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys18(yy358, yy359, yy360) → []
new_span2Ys5(:(Neg(Zero), yy3111)) → new_span2Ys12(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs5(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Zs19(yy364, yy365, yy366, yy384, yy383) → yy383
new_span2Zs7(:(Pos(Zero), yy3111)) → new_span2Zs110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_groupByZs01(Neg(Zero), :(Pos(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Ys17(yy358, yy359, yy360, Zero, Zero) → new_span2Ys16(yy358, yy359, yy360, new_span2Ys6(yy358, yy360), new_span2Zs6(yy358, yy360))
new_span2Zs11(yy376, yy377, yy378, Zero, Succ(yy3800)) → new_span2Zs12(yy376, yy377, yy378)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Zero) → new_span2Zs12(yy376, yy377, yy378)
new_span2Ys6(yy69, :(Pos(Zero), yy711)) → []
new_groupByZs06(yy183, yy184, yy185) → :(Pos(Succ(yy184)), yy185)
new_span2Zs11(yy376, yy377, yy378, Zero, Zero) → new_span2Zs13(yy376, yy377, yy378, new_span2Ys4(yy376, yy378), new_span2Zs4(yy376, yy378))
new_span2Zs4(yy82, :(Pos(yy8300), yy831)) → :(Pos(yy8300), yy831)
new_span2Zs6(yy76, :(Neg(yy7700), yy771)) → :(Neg(yy7700), yy771)
new_span2Zs5(:(Neg(Zero), yy3111)) → new_span2Zs17(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_groupByZs01(Pos(Zero), :(Neg(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Zs12(yy376, yy377, yy378) → :(Neg(Succ(yy377)), yy378)
new_span2Ys7(:(Pos(Zero), yy3111)) → new_span2Ys19(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys5([]) → []
new_groupByZs05(yy183, yy184, yy185, Zero, Zero) → new_groupByZs07(yy183, yy184, yy185, new_span2Ys6(yy183, yy185), new_span2Zs6(yy183, yy185))
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Zero) → new_groupByZs02(yy189, yy190, yy191)
new_groupByZs03(yy189, yy190, yy191, Zero, Succ(yy1930)) → new_groupByZs02(yy189, yy190, yy191)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys13(yy370, yy371, yy372, yy3730, yy3740)
new_span2Zs7([]) → []
new_groupByZs04(yy189, yy190, yy191, yy201, yy200) → yy200
new_span2Ys12(yy3111, yy7, yy6) → :(Neg(Zero), yy7)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs11(yy376, yy377, yy378, yy3790, yy3800)
new_span2Ys4(yy66, []) → []
new_span2Ys7([]) → []
new_span2Zs18(yy364, yy365, yy366) → :(Pos(Succ(yy365)), yy366)
new_groupByZs01(Neg(Succ(yy3000)), :(Pos(yy3100), yy311)) → :(Pos(yy3100), yy311)
new_span2Zs4(yy82, []) → []
new_span2Ys5(:(Pos(Zero), yy3111)) → new_span2Ys11(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs6(yy76, []) → []
new_span2Ys13(yy370, yy371, yy372, Zero, Zero) → new_span2Ys15(yy370, yy371, yy372, new_span2Ys4(yy370, yy372), new_span2Zs4(yy370, yy372))
new_span2Ys7(:(Pos(Succ(yy311000)), yy3111)) → []
new_groupByZs07(yy183, yy184, yy185, yy199, yy198) → yy198
new_span2Zs6(yy76, :(Pos(Zero), yy771)) → :(Pos(Zero), yy771)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Succ(yy31000)), yy311)) → new_groupByZs05(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Zs5(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs01(Neg(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Zero), yy311)) → :(Pos(Zero), yy311)
new_span2Ys5(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Ys14(yy370, yy371, yy372) → []
new_groupByZs01(Pos(Zero), :(Pos(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Ys4(yy66, :(Neg(Zero), yy671)) → []
new_span2Zs15(yy3111, yy19, yy18) → yy18
new_groupByZs01(Pos(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)

The set Q consists of the following terms:

new_span2Zs15(x0, x1, x2)
new_span2Zs7([])
new_span2Zs14(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys17(x0, x1, x2, Zero, Succ(x3))
new_span2Ys6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys12(x0, x1, x2)
new_span2Zs4(x0, [])
new_span2Zs18(x0, x1, x2)
new_span2Zs11(x0, x1, x2, Zero, Succ(x3))
new_span2Zs110(x0, x1, x2)
new_span2Zs7(:(Pos(Succ(x0)), x1))
new_span2Ys14(x0, x1, x2)
new_span2Zs5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Succ(x3), Zero)
new_span2Ys5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Zero, Zero)
new_span2Zs19(x0, x1, x2, x3, x4)
new_span2Ys7([])
new_span2Ys11(x0, x1, x2)
new_groupByZs01(Pos(Zero), :(Pos(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Succ(x3))
new_span2Zs7(:(Neg(Zero), x0))
new_span2Zs14(x0, x1, x2, Succ(x3), Zero)
new_span2Ys110(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Zero), :(Pos(Zero), x0))
new_groupByZs07(x0, x1, x2, x3, x4)
new_span2Zs5(:(Neg(Succ(x0)), x1))
new_groupByZs02(x0, x1, x2)
new_span2Ys7(:(Pos(Succ(x0)), x1))
new_span2Ys4(x0, :(Pos(x1), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Neg(Zero), x0))
new_span2Zs13(x0, x1, x2, x3, x4)
new_span2Ys16(x0, x1, x2, x3, x4)
new_span2Zs4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys7(:(Neg(Succ(x0)), x1))
new_span2Ys7(:(Neg(Zero), x0))
new_span2Ys17(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Succ(x0)), :(Pos(x1), x2))
new_groupByZs01(Neg(Succ(x0)), :(Neg(Succ(x1)), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Succ(x4))
new_groupByZs05(x0, x1, x2, Zero, Succ(x3))
new_span2Ys5(:(Neg(Zero), x0))
new_span2Ys19(x0, x1, x2)
new_span2Zs5(:(Pos(Zero), x0))
new_groupByZs01(Pos(Succ(x0)), :(Pos(Zero), x1))
new_groupByZs05(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys4(x0, :(Neg(Zero), x1))
new_span2Ys5(:(Neg(Succ(x0)), x1))
new_groupByZs01(Neg(Zero), :(Neg(Succ(x0)), x1))
new_span2Ys6(x0, [])
new_groupByZs01(Neg(Succ(x0)), :(Neg(Zero), x1))
new_span2Ys6(x0, :(Neg(x1), x2))
new_span2Zs12(x0, x1, x2)
new_groupByZs01(Neg(Zero), :(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Zero)
new_span2Zs11(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs16(x0, x1, x2)
new_span2Ys5(:(Pos(Zero), x0))
new_span2Ys6(x0, :(Pos(Zero), x1))
new_span2Zs17(x0, x1, x2)
new_span2Ys4(x0, [])
new_groupByZs01(x0, [])
new_span2Zs4(x0, :(Pos(x1), x2))
new_span2Zs6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys13(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys5([])
new_span2Zs6(x0, [])
new_span2Ys7(:(Pos(Zero), x0))
new_span2Ys17(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Neg(Zero), :(Pos(Succ(x0)), x1))
new_span2Ys17(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs4(x0, :(Neg(Zero), x1))
new_groupByZs06(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Succ(x0)), :(Neg(x1), x2))
new_span2Zs14(x0, x1, x2, Zero, Succ(x3))
new_groupByZs01(Pos(Zero), :(Neg(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Zero)
new_span2Ys13(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Pos(Zero), x0))
new_span2Zs5([])
new_span2Zs7(:(Pos(Zero), x0))
new_span2Ys15(x0, x1, x2, x3, x4)
new_groupByZs01(Pos(Succ(x0)), :(Pos(Succ(x1)), x2))
new_span2Zs14(x0, x1, x2, Zero, Zero)
new_groupByZs04(x0, x1, x2, x3, x4)
new_span2Zs6(x0, :(Pos(Zero), x1))
new_span2Zs6(x0, :(Neg(x1), x2))
new_span2Ys4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys18(x0, x1, x2)
new_span2Zs7(:(Neg(Succ(x0)), x1))
new_span2Zs5(:(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Succ(x3))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.